\begin{tabbing}
$\forall$${\it es}$:ES, $l$:IdLnk, ${\it tg}$:Id, $T$:Type.
\\[0ex](\{$m$\=:Msg$\mid$ source(mlnk($m$)) = source($l$) $\in$ Id\} \+
\\[0ex]$\subseteq$r Msg($\lambda$${\it l'}$,${\it tg'}$. if ${\it l'}$ = $l$ $\wedge_{b}$ ${\it tg'}$ = ${\it tg}$ then $T$ else Top fi ))
\-\\[0ex]$\Rightarrow$ ($\forall$$e$:E. ($\uparrow$isrcv($e$)) $\Rightarrow$ (lnk($e$) = $l$) $\Rightarrow$ (tag($e$) = ${\it tg}$) $\Rightarrow$ (valtype($e$) $\subseteq$r $T$))
\end{tabbing}